Left Termination of the query pattern
qplan(g,a)
w.r.t. the given Prolog program could successfully be proven:

(0) Obligation:

Clauses:

qplan(:-(P, Q), :-(P1, Q1)) :- ','(qplan(P, Q, P1, Q1), !).
qplan(P, P).
qplan(X0, P0, X, P) :- ','(numbervars(X0, 0, I), ','(variables(X0, 0, Vg), ','(numbervars(P0, I, N), ','(mark(P0, L, 0, Vl), ','(schedule(L, Vg, P1), ','(quantificate(Vl, 0, P1, P2), ','(functor(VA, $, N), ','(variablise(X0, VA, X), variablise(P2, VA, P))))))))).
mark(^(X, P), L, Q0, Q) :- ','(!, ','(variables(X, Q0, Q1), mark(P, L, Q1, Q))).
mark(','(P1, P2), L, Q0, Q) :- ','(!, ','(mark(P1, L1, Q0, Q1), ','(mark(P2, L2, Q1, Q), recombine(L1, L2, L)))).
mark(\+(P), L, Q, Q) :- ','(!, ','(mark(P, L0, 0, Vl), negate(L0, Vl, L))).
mark(SQ, .(m(V, C, SQ1), []), Q0, Q0) :- ','(subquery(SQ, SQ1, X, P, N, Q), ','(!, ','(mark(P, L, 0, Vl), ','(=(L, .(Q, [])), ','(marked(Q, Vq, C0, X4), ','(variables(X, Vl, Vlx), ','(setminus(Vq, Vlx, V0), ','(setofcost(V0, C0, C), variables(N, V0, V))))))))).
mark(P, .(m(V, C, P), []), Q, Q) :- ','(variables(P, 0, V), cost(P, V, C)).
subquery(setof(X, P, S), setof(X, Q, S), X, P, S, Q).
subquery(numberof(X, P, N), numberof(X, Q, N), X, P, N, Q).
negate([], X5, []).
negate(.(P, L), Vl, .(m(Vg, C, \+(P)), L1)) :- ','(freevars(P, V), ','(setminus(V, Vl, Vg), ','(negationcost(Vg, C), negate(L, Vl, L1)))).
negationcost(0, 0) :- !.
negationcost(V, 1000).
setofcost(0, X6, 0) :- !.
setofcost(X7, C, C).
variables('$MYVAR'(N), V0, V) :- ','(!, setplusitem(V0, N, V)).
variables(T, V, V) :- ','(atomic(T), !).
variables(T, V0, V) :- ','(functor(T, X8, N), variables(N, T, V0, V)).
variables(0, X9, V, V) :- !.
variables(N, T, V0, V) :- ','(is(N1, -(N, 1)), ','(arg(N, T, X), ','(variables(X, V0, V1), variables(N1, T, V1, V)))).
quantificate(-(W, V), N, P0, P) :- ','(!, ','(is(N1, +(N, 18)), ','(quantificate(V, N, P1, P), quantificate(W, N1, P0, P1)))).
quantificate(0, X10, P, P) :- !.
quantificate(V, N, P0, ^('$MYVAR'(Nr), P)) :- ','(is(Vr, /\(V, -(V))), ','(log2(Vr, I), ','(is(Nr, +(N, I)), ','(is(N1, +(Nr, 1)), ','(is(V1, >>(V, +(I, 1))), quantificate(V1, N1, P0, P)))))).
log2(1, 0) :- !.
log2(2, 1) :- !.
log2(4, 2) :- !.
log2(8, 3) :- !.
log2(N, I) :- ','(is(N1, >>(N, 4)), ','(=\=(N1, 0), ','(log2(N1, I1), is(I, +(I1, 4))))).
schedule(.(P, []), Vg, Q) :- ','(!, schedule1(P, Vg, Q)).
schedule(.(P1, P2), Vg, ','(Q1, Q2)) :- ','(!, ','(schedule1(P1, Vg, Q1), schedule(P2, Vg, Q2))).
schedule1(m(V, C, P), Vg, Q) :- ','(maybe_cut(V, Vg, Q0, Q), plan(P, V, C, Vg, Q0)).
maybe_cut(V, Vg, P, {}(P)) :- ','(disjoint(V, Vg), !).
maybe_cut(V, Vg, P, P).
plan(\+(P), Vg, X11, X12, \+(Q)) :- ','(!, ','(=(Vg, 0), ','(marked(P, V, C, P1), ','(plan(P1, V, C, Vg, Q1), quantificate(V, 0, Q1, Q))))).
plan(SQ, Vg, X13, X14, SQ1) :- ','(subquery(SQ, SQ1, X, P, X15, Q), ','(!, ','(marked(P, V, C, P1), ','(variables(X, Vg, Vgx), ','(setminus(V, Vgx, Vl), ','(quantificate(Vl, 0, Q1, Q), plan(P1, V, C, Vgx, Q1))))))).
plan(P, V, C, Vg, ','(Q, R)) :- ','(is_conjunction(P), ','(!, ','(best_goal(P, V, C, P0, V0, PP), ','(plan(P0, V0, C, Vg, Q), ','(instantiate(PP, V0, L), ','(add_keys(L, L1), ','(keysort(L1, L2), ','(strip_keys(L2, L3), schedule(L3, Vg, R))))))))).
plan(P, X16, X17, X18, P).
is_conjunction(','(X19, X20)).
marked(m(V, C, P), V, C, P).
freevars(m(V, X21, X22), V).
best_goal(','(P1, P2), V, C, P0, V0, m(V, C, Q)) :- ','(!, ','(;(','(marked(P1, Va, C, Pa), =(Q, ','(Pb, P2))), ','(marked(P2, Va, C, Pa), =(Q, ','(P1, Pb)))), ','(!, best_goal(Pa, Va, C, P0, V0, Pb)))).
best_goal(P, V, C, P, V, true).
instantiate(true, X23, []) :- !.
instantiate(P, Vi, .(P, [])) :- ','(freevars(P, V), ','(disjoint(V, Vi), !)).
instantiate(m(V, X24, P), Vi, L) :- instantiate0(P, V, Vi, L).
instantiate0(','(P1, P2), X25, Vi, L) :- ','(instantiate(P1, Vi, L1), ','(instantiate(P2, Vi, L2), recombine(L1, L2, L))).
instantiate0(\+(P), V, Vi, L) :- ','(!, ','(instantiate(P, Vi, L0), ','(freevars(P, Vf), ','(setminus(Vf, V, Vl), negate(L0, Vl, L))))).
instantiate0(SQ, Vg, Vi, .(m(V, C, SQ1), [])) :- ','(subquery(SQ, SQ1, X, P, X26, Q), ','(!, ','(instantiate(P, Vi, L), ','(=(L, .(Q, [])), ','(marked(Q, Vq, C0, X27), ','(setminus(Vg, Vi, V), ','(variables(X, 0, Vx), ','(setminus(V, Vx, V0), setofcost(V0, C0, C))))))))).
instantiate0(P, V, Vi, .(m(V1, C, P), [])) :- ','(setminus(V, Vi, V1), cost(P, V1, C)).
recombine(L, [], L) :- !.
recombine([], L, L).
recombine(.(P1, L1), .(P2, L2), L) :- ','(marked(P1, V1, C1, X28), ','(nonempty(V1), ','(incorporate(P1, V1, C1, P2, L2, L3), ','(!, recombine(L1, L3, L))))).
recombine(.(P, L1), L2, .(P, L)) :- recombine(L1, L2, L).
incorporate(P0, V0, C0, P1, L1, L) :- ','(marked(P1, V1, C1, X29), ','(intersect(V0, V1), ','(!, ','(setplus(V0, V1, V), ','(minimum(C0, C1, C), incorporate0(m(V, C, ','(P0, P1)), V, C, L1, L)))))).
incorporate(P0, V0, C0, P1, .(P2, L1), .(P1, L)) :- incorporate(P0, V0, C0, P2, L1, L).
incorporate0(P0, V0, C0, .(P1, L1), L) :- ','(incorporate(P0, V0, C0, P1, L1, L), !).
incorporate0(P, X30, X31, L, .(P, L)).
minimum(N1, N2, N1) :- ','(=<(N1, N2), !).
minimum(N1, N2, N2).
add_keys([], []).
add_keys(.(P, L), .(-(C, P), L1)) :- ','(marked(P, X32, C, X33), add_keys(L, L1)).
strip_keys([], []).
strip_keys(.(X, L), .(P, L1)) :- ','(strip_key(X, P), strip_keys(L, L1)).
strip_key(-(C, P), P).
variablise('$MYVAR'(N), VV, V) :- ','(!, ','(is(N1, +(N, 1)), arg(N1, VV, V))).
variablise(T, X34, T) :- ','(atomic(T), !).
variablise(T, VV, T1) :- ','(functor(T, F, N), ','(functor(T1, F, N), variablise(N, T, VV, T1))).
variablise(0, X35, X36, X37) :- !.
variablise(N, T, VV, T1) :- ','(is(N1, -(N, 1)), ','(arg(N, T, X), ','(arg(N, T1, X1), ','(variablise(X, VV, X1), variablise(N1, T, VV, T1))))).
cost(+(P), 0, N) :- ','(!, cost(P, 0, N)).
cost(+(P), V, 1000) :- !.
cost(P, V, N) :- ','(functor(P, F, I), cost(I, F, P, V, N)).
cost(1, F, P, V, N) :- ','(arg(1, P, X1), ','(instantiated(X1, V, I1), ','(nd(F, N0, N1), is(N, -(N0, *(I1, N1)))))).
cost(2, F, P, V, N) :- ','(arg(1, P, X1), ','(instantiated(X1, V, I1), ','(arg(2, P, X2), ','(instantiated(X2, V, I2), ','(nd(F, N0, N1, N2), is(N, -(N0, -(*(I1, N1), *(I2, N2))))))))).
cost(3, F, P, V, N) :- ','(arg(1, P, X1), ','(instantiated(X1, V, I1), ','(arg(2, P, X2), ','(instantiated(X2, V, I2), ','(arg(3, P, X3), ','(instantiated(X3, V, I3), ','(nd(F, N0, N1, N2, N3), is(N, -(N0, -(*(I1, N1), -(*(I2, N2), *(I3, N3)))))))))))).
instantiated(.(X, X38), V, N) :- ','(!, instantiated(X, V, N)).
instantiated('$MYVAR'(N), V, 0) :- ','(setcontains(V, N), !).
instantiated(X39, X40, 1).
nonempty(0) :- ','(!, fail).
nonempty(X41).
setplus(-(W1, V1), -(W2, V2), -(W, V)) :- ','(!, ','(is(V, \/(V1, V2)), setplus(W1, W2, W))).
setplus(-(W, V1), V2, -(W, V)) :- ','(!, is(V, \/(V1, V2))).
setplus(V1, -(W, V2), -(W, V)) :- ','(!, is(V, \/(V1, V2))).
setplus(V1, V2, V) :- is(V, \/(V1, V2)).
setminus(-(W1, V1), -(W2, V2), S) :- ','(!, ','(is(V, /\(V1, \(V2))), ','(setminus(W1, W2, W), mkset(W, V, S)))).
setminus(-(W, V1), V2, -(W, V)) :- ','(!, is(V, /\(V1, \(V2)))).
setminus(V1, -(W, V2), V) :- ','(!, is(V, /\(V1, \(V2)))).
setminus(V1, V2, V) :- is(V, /\(V1, \(V2))).
mkset(0, V, V) :- !.
mkset(W, V, -(W, V)).
setplusitem(-(W, V), N, -(W, V1)) :- ','(<(N, 18), ','(!, is(V1, \/(V, <<(1, N))))).
setplusitem(-(W, V), N, -(W1, V)) :- ','(!, ','(is(N1, -(N, 18)), setplusitem(W, N1, W1))).
setplusitem(V, N, V1) :- ','(<(N, 18), ','(!, is(V1, \/(V, <<(1, N))))).
setplusitem(V, N, -(W, V)) :- ','(is(N1, -(N, 18)), setplusitem(0, N1, W)).
setcontains(-(W, V), N) :- ','(<(N, 18), ','(!, =\=(/\(V, <<(1, N)), 0))).
setcontains(-(W, V), N) :- ','(!, ','(is(N1, -(N, 18)), setcontains(W, N1))).
setcontains(V, N) :- ','(<(N, 18), =\=(/\(V, <<(1, N)), 0)).
intersect(-(W1, V1), -(W2, V2)) :- ','(!, ','(;(=\=(/\(V1, V2), 0), intersect(W1, W2)), !)).
intersect(-(W, V1), V2) :- ','(!, =\=(/\(V1, V2), 0)).
intersect(V1, -(W, V2)) :- ','(!, =\=(/\(V1, V2), 0)).
intersect(V1, V2) :- =\=(/\(V1, V2), 0).
disjoint(-(W1, V1), -(W2, V2)) :- ','(!, ','(=:=(/\(V1, V2), 0), disjoint(W1, W2))).
disjoint(-(W, V1), V2) :- ','(!, =:=(/\(V1, V2), 0)).
disjoint(V1, -(W, V2)) :- ','(!, =:=(/\(V1, V2), 0)).
disjoint(V1, V2) :- =:=(/\(V1, V2), 0).
nd(african, 19, 26).
nd(american, 19, 26).
nd(area, 51, 51).
nd(area, 22, 22, 51).
nd(asian, 21, 26).
nd(aggregate, 103, 3, 100, 51).
nd(one_of, 99, 200, -99).
nd(ratio, 99, 51, 51, 3).
nd(card, 99, 100, 3).
nd(borders, 29, 22, 22).
nd(capital, 22, 22).
nd(capital, 22, 22, 23).
nd(city, 18, 18).
nd(continent, 8, 8).
nd(country, 22, 22).
nd(drains, 16, 16, 10).
nd(eastof, 40, 22, 22).
nd(european, 19, 26).
nd(exceeds, 99, 51, 51).
nd(flows, 19, 16, 22).
nd(flows, 19, 16, 22, 22).
nd(in, 29, 26, 15).
nd(latitude, 23, 23).
nd(latitude, 22, 22, 23).
nd(longitude, 26, 26).
nd(longitude, 22, 22, 26).
nd(northof, 40, 22, 22).
nd(ocean, 7, 7).
nd(population, 51, 51).
nd(population, 23, 23, 51).
nd(region, 12, 12).
nd(rises, 16, 16, 22).
nd(river, 16, 16).
nd(sea, 8, 8).
nd(place, 23, 23).
nd(seamass, 10, 10).
nd(southof, 40, 22, 22).
nd(westof, 40, 22, 22).
nd(=<, 99, 51, 51).
nd(<, 99, 51, 51).
nd(>, 99, 51, 51).
nd(>=, 99, 51, 51).

Query: qplan(g,a)

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph DT10.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="A: qplan(T2, T3)\n\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
2 [label="2: qplan(T2, T3), SCOPE: 1, CLAUSE: 0 | qplan(T2, T3), SCOPE: 1, CLAUSE: 1\n\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
3 [label="3: ','(qplan(T8, T9, T12, T13), !_1) | qplan(:-(T8, T9), T3), SCOPE: 1, CLAUSE: 1\n\nT8 is ground\nT9 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
4 [label="4: qplan(T2, T3), SCOPE: 1, CLAUSE: 1\n\nT2 is ground\nX46 is free\nX47 is free\nX48 is free\nX49 is free\nqplan(T2, T3) !=? qplan(:-(X46, X47), :-(X48, X49))", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: ','(qplan(T8, T9, T12, T13), !_1), SCOPE: 2, CLAUSE: 2 | ?_2 | qplan(:-(T8, T9), T3), SCOPE: 1, CLAUSE: 1\n\nT8 is ground\nT9 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: ','(','(numbervars(T24, 0, X70), ','(variables(T24, 0, X71), ','(numbervars(T25, X70, X72), ','(mark(T25, X73, 0, X74), ','(schedule(X73, X71, X75), ','(quantificate(X74, 0, X75, X76), ','(functor(X77, $, X72), ','(variablise(T24, X77, T28), variablise(X76, X77, T29))))))))), !_1) | ?_2 | qplan(:-(T24, T25), T3), SCOPE: 1, CLAUSE: 1\n\nT24 is ground\nT25 is ground\nX70 is free\nX71 is free\nX72 is free\nX73 is free\nX74 is free\nX75 is free\nX76 is free\nX77 is free", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 11 [arrowhead = none ];
11 -> 2;

12 [label="EVAL with clause\nqplan(:-(X46, X47), :-(X48, X49)) :- ','(qplan(X46, X47, X48, X49), !_1).\nand substitutionX46 -> T8,\nX47 -> T9,\nT2 -> :-(T8, T9),\nX48 -> T12,\nX49 -> T13,\nT3 -> :-(T12, T13),\nT10 -> T12,\nT11 -> T13", fontsize=14, style = filled, fillcolor = lightblue];
2 -> 12 [arrowhead = none ];
12 -> 3;

13 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
2 -> 13 [arrowhead = none ];
13 -> 4;

14 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
3 -> 14 [arrowhead = none ];
14 -> 5;

15 [label="EVAL with clause\nqplan(X79, X79).\nand substitutionT2 -> T31,\nX79 -> T31,\nT3 -> T31", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 15 [arrowhead = none ];
15 -> 8;

16 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
4 -> 16 [arrowhead = none ];
16 -> 9;

17 [label="ONLY EVAL with clause\nqplan(X66, X67, X68, X69) :- ','(numbervars(X66, 0, X70), ','(variables(X66, 0, X71), ','(numbervars(X67, X70, X72), ','(mark(X67, X73, 0, X74), ','(schedule(X73, X71, X75), ','(quantificate(X74, 0, X75, X76), ','(functor(X77, $, X72), ','(variablise(X66, X77, X68), variablise(X76, X77, X69))))))))).\nand substitutionT8 -> T24,\nX66 -> T24,\nT9 -> T25,\nX67 -> T25,\nT12 -> T28,\nX68 -> T28,\nT13 -> T29,\nX69 -> T29,\nT26 -> T28,\nT27 -> T29", fontsize=14, style = filled, fillcolor = lightblue];
5 -> 17 [arrowhead = none ];
17 -> 6;

18 [label="UNDEFINED ERROR", fontsize=14, style = filled, fillcolor = lightgreen];
6 -> 18 [arrowhead = none ];
18 -> 7;

19 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
8 -> 19 [arrowhead = none ];
19 -> 10;

}

(2) Obligation:

Triples:


Clauses:


Afs:

(3) TPisEmptyProof (EQUIVALENT transformation)

There are no more dependency triples. Hence, the dependency triple problem trivially terminates.

(4) YES